package test.logic.nfm;

import static org.junit.Assert.assertEquals;
import static org.junit.Assert.assertNotNull;
import static org.junit.Assert.assertNull;
import static org.junit.Assert.assertTrue;

import java.util.Collections;
import java.util.HashSet;
import java.util.LinkedList;
import java.util.List;
import java.util.Set;

import org.apache.log4j.ConsoleAppender;
import org.apache.log4j.Logger;
import org.junit.After;
import org.junit.Before;
import org.junit.BeforeClass;
import org.junit.Test;

import cfsmon.common.Event;
import cfsmon.core.LogConfig;
import cfsmon.logic.dfm.DfmState;
import cfsmon.logic.dfm.IDfm;
import cfsmon.logic.nfm.INfm;
import cfsmon.logic.nfm.Nfm;
import cfsmon.logic.nfm.NfmState;
import cfsmon.logic.nfm.NfmToDfmTranslator;

public class NfmToDfmTranslator01 {

	private INfm nfm;
	
	@BeforeClass
	public static void classSetUp(){
		Logger.getRootLogger().removeAllAppenders();
		Logger.getRootLogger().addAppender(new ConsoleAppender(LogConfig.cfsmonLogConsoleLayout));
	}
	
	@Test
	public void testNull() {
		IDfm dfm = NfmToDfmTranslator.translateToDfm(null);
		assertNull(dfm);
	}

	@Before
	public void setUp() throws Exception {
		nfm = new Nfm();
	}
	
	@After
	public void tearDown() throws Exception {
		nfm = null;
	}
	
	@Test
	public void testInput01(){
		/*
		 * L = (e0 e0 | e1 e1)+ (e0 | e1)?
		 */
		NfmState s0, s1, s2, s3;
		Event e0, e1;
		s0 = new NfmState("s0");
		s1 = new NfmState("s1");
		s2 = new NfmState("s2");
		s3 = new NfmState("s3");
		e0 = new Event("e0");
		e1 = new Event("e1");
		
		s0.putTransition(e0, s1);
		s0.putTransition(e1, s2);
		
		s1.putTransition(e0, s0);
		s1.addDefaultTransition(s3);
		s2.putTransition(e1, s0);
		s2.addDefaultTransition(s3);
		
		nfm.addInitialState(s0);
		nfm.addState(s1);
		nfm.addState(s2);
		nfm.addFinalState(s3);
		nfm.addEvent(e0);
		nfm.addEvent(e1);
		
		IDfm dfm = NfmToDfmTranslator.translateToDfm(nfm);

		List<Event> word01 = new LinkedList<Event>();
		word01.add(e0); // accepts
		assertTrue(inputEquivalent(nfm, dfm, word01));
		
		List<Event> word02 = new LinkedList<Event>();
		word02.add(e0); word02.add(e1); // rejects
		assertTrue(inputEquivalent(nfm, dfm, word02));
		
		List<Event> word03 = new LinkedList<Event>();
		word03.add(e0); word03.add(e0);
		word03.add(e1); word03.add(e1); // accepts
		assertTrue(inputEquivalent(nfm, dfm, word03));
		
		List<Event> word04 = new LinkedList<Event>();
		word04.add(e0); word04.add(e0);
		word04.add(e1); word04.add(e0);// rejects
		assertTrue(inputEquivalent(nfm, dfm, word04));
		
	}
	
	@Test
	public void testMinimalNfm(){

		NfmState s0;
		s0 = new NfmState("sx");
		s0.addDefaultTransition(s0);
		nfm.addInitialState(s0);
		nfm.addFinalState(s0);
		
		IDfm dfm = NfmToDfmTranslator.translateToDfm(nfm);
		
		DfmState ds0 = dfm.getStates().get("sx");
		assertEquals(dfm.getInitialState(), ds0);
		assertTrue(dfm.getFinalStates().contains(ds0));
		assertEquals(ds0.getDefaultTransition(), ds0);
	}
	
	@Test
	public void testDetWithoutStates(){
		IDfm dfm = NfmToDfmTranslator.translateToDfm(nfm);
		assertTrue(dfm.getStates().isEmpty());
		assertTrue(dfm.getFinalStates().isEmpty());
		assertNull(dfm.getInitialState());
	}
	
	@Test
	public void testDetWithoutEvents(){
		NfmState[] n = getSomeStates(2); // n[0] to n[1]
		nfm.addInitialState(n[0]);
		nfm.addFinalState(n[1]);
		n[0].addDefaultTransition(n[1]);
		
		IDfm dfm = NfmToDfmTranslator.translateToDfm(nfm);
		
		assertFmEqual(nfm, dfm);
	}
	
	@Test
	public void testDet(){
		NfmState[] n = getSomeStates(3); // n[0] to n[1]
		Event[] e = getSomeEvents(2); // e[0] to e[1]
		
		n[0].putTransition(e[0], n[1]);
		n[0].putTransition(e[1], n[2]);
		n[1].putTransition(e[0], n[2]);
		n[1].putTransition(e[1], n[0]);
		n[2].putTransition(e[0], n[0]);
		n[2].putTransition(e[1], n[1]);

		nfm.addEvent(e[0]);
		nfm.addEvent(e[1]);
		nfm.addInitialState(n[0]);
		nfm.addState(n[1]);
		nfm.addFinalState(n[2]);
		nfm.setMaximumNumberOfMonitors(2);
		
		IDfm dfm = NfmToDfmTranslator.translateToDfm(nfm);
		
		assertFmEqual(nfm, dfm);
	}
	
	@Test
	public void testUnreachableFinalState(){
		NfmState[] n = getSomeStates(3); // n[0] to n[2]
		n[0].addDefaultTransition(n[1]);
		n[1].addDefaultTransition(n[2]);
		
		nfm.addInitialState(n[0]);
		nfm.addState(n[1]);
		nfm.addFinalState(n[2]);
		
		IDfm dfm = NfmToDfmTranslator.translateToDfm(nfm);
		
		assertFmEqual(nfm, dfm);
	}
	
	private static void assertFmEqual(INfm nfm, IDfm dfm){
		// monitor number
		assertEquals(nfm.getMaximumNumberOfMonitors(), dfm.getMaximumNumberOfMonitors());
		// events
		assertTrue(nfm.getEvents().values().containsAll(dfm.getEvents().values()) &&
				dfm.getEvents().values().containsAll(nfm.getEvents().values()));
		// parameters
		assertTrue(nfm.getParameters().values().containsAll(dfm.getParameters().values()) &&
				dfm.getParameters().values().containsAll(nfm.getParameters().values()));
		// states and transitions
		assertEquals(nfm.getStates().values().size(), dfm.getStates().values().size());
		for (NfmState s : nfm.getStates().values()){
			DfmState d = dfm.getStates().get(s.getName());
			assertNotNull(d);
			for(Event e : s.getTransitions().keySet()){
				assertNotNull(d.getTransitions().get(e));
				for (NfmState se : s.getTransitions().get(e)){
					assertEquals(se.getName(), d.getTransitions().get(e).getName());					
				}
			}
			for (NfmState sdef : s.getDefaultTransition()){
				assertNotNull(d.getDefaultTransition());
				assertEquals(d.getDefaultTransition().getName(), sdef.getName());
			}
		}
		
	}

	@Test
	public void testNondet01(){
		NfmState[] n = getSomeStates(3); // n[0] to n[2]
		Event[] e = getSomeEvents(1); // e[0]

		n[0].putTransition(e[0], n[1]);
		n[0].putTransition(e[0], n[2]);
		
		nfm.addEvent(e[0]);
		nfm.addInitialState(n[0]);
		nfm.addState(n[1]);
		nfm.addFinalState(n[2]);
		
		IDfm dfm = NfmToDfmTranslator.translateToDfm(nfm);
		
		DfmState ds0 = dfm.getInitialState();
		assertTrue(dfm.getFinalStates().contains(ds0.getTransitions().get(e[0])));
		assertEquals(dfm.getFinalStates().size(), 1);
	}
	
	@Test
	public void testTwoInitialStatesNonTotal(){
		NfmState[] n = getSomeStates(3); // n[0] to n[2]
		Event[] e = getSomeEvents(2); // e[0] to e[1]
		n[0].putTransition(e[0], n[0]);
		n[0].addDefaultTransition(n[2]);
		n[1].putTransition(e[0], n[1]);
		n[1].addDefaultTransition(n[2]);
		
		nfm.addEvent(e[0]);
		nfm.addEvent(e[1]);
		nfm.addInitialState(n[0]);
		nfm.addInitialState(n[1]);
		nfm.addFinalState(n[2]);
		
		IDfm dfm = NfmToDfmTranslator.translateToDfm(nfm);
		
		assertEquals(3, dfm.getStates().values().size());
	}
	
	@Test
	public void testTwoInitialStatesTotal(){
		NfmState[] n = getSomeStates(3); // n[0] to n[2]
		Event[] e = getSomeEvents(2); // e[0] to e[1]
		n[0].putTransition(e[0], n[0]);
		n[0].addDefaultTransition(n[2]);
		n[1].putTransition(e[0], n[1]);
		n[1].addDefaultTransition(n[2]);
		n[2].addDefaultTransition(n[2]);
		
		nfm.addEvent(e[0]);
		nfm.addEvent(e[1]);
		nfm.addInitialState(n[0]);
		nfm.addInitialState(n[1]);
		nfm.addFinalState(n[2]);
		
		IDfm dfm = NfmToDfmTranslator.translateToDfm(nfm);
		
		assertEquals(2, dfm.getStates().values().size());
	}
	
	@Test
	public void testIndetDefault(){
		NfmState[] n = getSomeStates(3); // n[0] to n[2]
		Event[] e = getSomeEvents(1); // e[0]
		n[0].addDefaultTransition(n[1]);
		n[0].addDefaultTransition(n[2]);
		n[1].addDefaultTransition(n[1]);
		n[2].addDefaultTransition(n[2]);
		
		nfm.addEvent(e[0]);
		nfm.addInitialState(n[0]);
		nfm.addFinalState(n[1]);
		nfm.addFinalState(n[2]);
		
		IDfm dfm = NfmToDfmTranslator.translateToDfm(nfm);
		
		assertEquals(2, dfm.getStates().values().size());
	}
	
	private NfmState[] getSomeStates(int amount){
		NfmState[] n = new NfmState[amount];
		for (int i = 0; i < n.length; i++)
			n[i] = new NfmState("n" + i);
		return n;
	}
	
	private Event[] getSomeEvents(int amount){
		Event[] e = new Event[amount];
		for (int i = 0; i < e.length; i++)
			e[i] = new Event("e" + i);
		return e;
	}
	
	private boolean inputEquivalent(INfm nfm, IDfm dfm, List<Event> word){
		if (nfm == null && dfm == null){
			return true;			
		} else if (nfm == null || dfm == null ) {
			return false;
		} else {
			NfmInstance ni = new NfmInstance(nfm);
			DfmInstance di = new DfmInstance(dfm);
			return ni.accepts(word) == di.accepts(word);			
		}
	}
	
	private class NfmInstance{
		private INfm nfm;
		private Set<NfmState> currentState;
		
		public NfmInstance(INfm nfm){
			this.nfm = nfm;
			currentState = new HashSet<NfmState>();
			currentState.addAll(nfm.getInitialStates());
		}
		
		public boolean accepts(List<Event> word){
			
			for (Event e : word){
				if (isFinal())
					return true;
				else
					move(e);
			}
			return isFinal();
		}
		
		private boolean isFinal(){
			return (!Collections.disjoint(nfm.getFinalStates(), currentState));
		}
		
		private void move(Event e){
			Set<NfmState> nextState = new HashSet<NfmState>();
			for (NfmState from : currentState){
				if( from.getTransitions().get(e) == null ||
						from.getTransitions().get(e).isEmpty()){
					nextState.addAll(from.getDefaultTransition());
				} else {
					nextState.addAll(from.getTransitions().get(e));
				}
			}
			currentState = nextState;
		}
	}
	
	private class DfmInstance{
		private IDfm dfm;
		private DfmState currentState;
		
		public DfmInstance(IDfm dfm){
			this.dfm = dfm;
			currentState = dfm.getInitialState();
		}
		
		public boolean accepts(List<Event> word){
			
			for (Event e : word){
				if (isFinal())
					return true;
				else
					move(e);
			}
			return isFinal();
		}
		
		private boolean isFinal(){
			return (dfm.getFinalStates().contains(currentState));
		}
		
		private void move(Event e){
			
			DfmState nextState = currentState.getTransitions().get(e);
			if (nextState == null)
				nextState = currentState.getDefaultTransition();
			currentState = nextState;
		}
	}

}
